specification
using nat
constants ENCODED_ELEM_ALIGNMENT : nat;
axioms alignment-not-zero : ⊦ ENCODED_ELEM_ALIGNMENT ≠ 0;
used for: s, ls;
end specification